Nuprl Definition : es-trans-state-from
11,40
postcript
pdf
es-trans-state-from{i:l}(
es
;
ks
;
g
;
z
;
e1
;
e2
)
== list_accum(
x
,
a
.spreadn(
a
;
k
,
s
,
v
.if deq-member(Kind-deq;
k
;
ks
) then
g
(
k
,
s
,
v
,
x
) else
x
fi );
== list_accum(
z
;
== list_accum(
es-hist{i:l}(
es
;
e1
;
e2
))
latex
clarification:
es-trans-state-from{i:l}
es-trans-state-from
(
es
;
ks
;
g
;
z
;
e1
;
e2
)
== list_accum(
x
,
a
.spreadn(
a
;
k
,
s
,
v
.if deq-member(Kind-deq;
k
;
ks
) then
g
(
k
,
s
,
v
,
x
) else
x
fi );
== list_accum(
z
;
== list_accum(
es-hist{i:l}
== list_accum(es-hist
(
es
;
e1
;
e2
))
latex
Definitions
list_accum(
x
,
a
.
f
(
x
;
a
);
y
;
l
)
,
spreadn(
a
;
x
,
y
,
z
.
t
(
x
;
y
;
z
))
,
if
b
then
t
else
f
fi
,
deq-member(
eq
;
x
;
L
)
,
Kind-deq
,
es-hist{i:l}(
es
;
e1
;
e2
)
FDL editor aliases
es-trans-state-from
origin